Nuprl Lemma : es-interface-conditional-domain-member
11,40
postcript
pdf
es
:ES,
A
:Type,
I1
,
I2
:AbsInterface(
A
),
e
:E.
(
(
e
[
I1
?
I2
]))
((
(
e
I1
))
(
(
e
I2
)))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
t
T
,
,
T
,
True
,
P1
P2
,
P1
P2
,
{
I
}
Lemmas
assert
wf
,
es-is-interface
wf
,
es-E
wf
,
es-interface
wf
,
event
system
wf
,
es-interface-conditional-predicate-equivalent
,
es-interface-conditional
,
squash
wf
,
true
wf
,
bool
wf
,
es-interface-conditional-domain
,
assert
of
bor
origin